$\forall$$A$, $B$:Type. \\[0ex]($A$ $\subseteq$r $B$) $\Rightarrow$ ($\forall$$x$, $y$:$A$. ($x$ = $y$ $\in$ $B$) $\Rightarrow$ ($x$ = $y$)) $\Rightarrow$ (EqDecider($B$) $\subseteq$r EqDecider($A$))